g:IMonoid, n:, e:|g|. (n  e)  |g| 

latex

Up	groups 1
Definitions of Statement	IMonoid, n  e
Definitions	n  e, t  T, x:A. B(x), IMonoid
Lemmas	imon wf, nat wf, grp car wf, nat op wf